00100	VAR: x,y,z,u,v,w, X,Y,Z ,U;
00150	INF_PRED:=;PRE_PRED:B,D;
00200	EQUALITY: =;
00300	A1: B(x,y,z) ⊃ B(z,y,x);
00400	A2: B(x,y,z)∧B(y,w,z) ⊃ B(x,y,w);
00500	A3: D(x,y,y,x);
00600	A4: D(x,y,z,z)⊃ x=y;
00700	A5: D(x,y,u,v)∧D(x,y,z,w) ⊃ D(u,v,z,w);
00800	A6: ¬(x=y)∧B(x,y,z)∧B(X,Y,Z)∧D(x,y,X,Y)∧D(y,z,Y,Z)
00900	    ∧D(u,x,U,X)∧D(u,y,U,Y)⊃D(u,z,U,Z);
01000	A7: ∃(y)(B(u,x,y)∧D(x,y,z,w));
01100	A8: ∃(y)(B(x,y,z)∧D(x,y,y,z));
01200	A9: ∃(x,y,z)(¬B(x,y,z)∧¬B(y,z,x)∧¬B(z,x,y));
01300	A10: (¬(u=v)∧D(x,u,x,v)∧D(y,u,y,v)∧D(z,u,z,v))⊃
01400	    (B(x,y,z)∨B(y,z,x)∨B(z,x,y));
01500	A11:(¬B(x,y,z)∧¬B(y,z,x)∧B(z,x,y))⊃∃(u)(D(u,x,u,y)∧D(u,x,u,z));
01600	C:B(x,y,z)⊃∃(Z)(B(u,y,Z)∧D(x,Z,x,z));
01700	THEOREM: (B(U,w,u)∧B(x,U,y))⊃∃(X)(B(X,w,x)∧B(y,X,u));;